Search for: All records

We present the first formal-methods analysis of the Session Binding Proxy (SBP) protocol, which protects a vulnerable system by wrapping it and introducing a reverse proxy between the system and its clients. SBP mitigates thefts of authentication cookies by cryptographically binding the authentication cookie---issued by the server to the client---to an underlying Transport Layer Security (TLS) channel using the channel's master secret and a secret key known only by the proxy. An adversary who steals a bound cookie cannot reuse this cookie to create malicious requests on a separate connection because the cookie's channel binding will not match the adversary's channel. SBP seeks to achieve this goal without modifications to the client or the server software, rendering the client and server ``oblivious protocol participants'' that are not aware of the SBP session. Our analysis verifies that the original SBP design mitigates cookie stealing under the client's cryptographic assumptions but fails to authenticate the client to the proxy. Resulting from two issues, the proxy has no assurance that it shares a session context with a legitimate client: SBP assumes an older flawed version of TLS (1.2), and SBP relies on legacy server usernames and passwords to authenticate clients. Due to these issues, there is no guarantee of cookie-stealing resistance from the proxy's cryptographic perspective. Using the Cryptographic Protocol Shapes Analyzer (CPSA), we model and analyze the original SBP and three variations in the Dolev-Yao network intruder model. Our models differ in the version of TLS they use: 1.2 (original SBP), 1.2 with mutual authentication, 1.3, and {\it 1.3 with mutual authentication (mTLS-1.3)}. For comparison, we also analyze a model of the baseline scenario without SBP. We separately analyze each of our SBP models from two perspectives: client and proxy. In each SBP model, the client has assurance that the cookie is valid only for the client's legitimate session. Only in mTLS-1.3 does the proxy have assurance that it communicates with a legitimate client and that the client's cookie is valid. We formalize these results by stating and proving, or disproving, security goals for each model. SBP is useful because it provides a practical solution to the important challenge of protecting flawed legacy systems that cannot be patched. Our analysis of this obscure protocol sheds insight into the properties necessary for wrapper protocols to resist a Dolev-Yao adversary. When engineering wrapper protocols, designers must carefully consider authentication, freshness, and requirements of cryptographic bindings such as channel bindings. Our work exposes strengths and limitations of wrapper protocols and TLS channel bindings. 

s a case study in cryptographic binding, we present a formal-methods analysis of the Fast IDentity Online (FIDO) Universal Authentication Framework (UAF) authentication protocol's cryptographic channel binding mechanisms. First, we show that UAF's channel bindings fail to mitigate protocol interaction by a Dolev-Yao (DY) adversary, enabling the adversary to transfer the server's authentication challenge to alternate sessions of the protocol. As a result, in some contexts, the adversary can masquerade as a client and establish an authenticated session with a server, which might be a bank server. Second, we implement a proof-of-concept man-in-the-middle attack against eBay's open source FIDO UAF implementation. Third, we propose and verify an improvement of UAF channel binding that better resists protocol interaction, in which the client and the server, rather than the client alone, bind the server's challenge to the session. The weakness we analyze is similar to the vulnerability discovered in the Needham-Schroeder protocol over 25 years ago. That this vulnerability appears in FIDO UAF highlights the strong need for protocol designers to bind messages properly and to analyze their designs with formal-methods tools. UAF's channel bindings fail for four reasons: channel binding is optional; the client cannot authenticate the server's challenge, even when channel binding is used; the standard permits the server to accept incorrect channel bindings; and the protocol binds only to the communication endpoints and not to the protocol session. We carry out our analysis of the standard and our suggested improvement using the Cryptographic Protocol Shapes Analyzer (CPSA). To our knowledge, we are first to carry out a formal-methods analysis of channel binding in FIDO UAF, first to identify the structural weakness resulting from improper binding, and first to exhibit details of an attack resulting from this weakness. In FIDO UAF, the client can cryptographically bind protocol data (including a server-generated authentication challenge) to the underlying authenticated communication channel. To facilitate the protocol's adoption, the FIDO Alliance makes the channel binding optional and allows a server to accept incorrect channel bindings, such as when the client communicates through a network perimeter proxy. Practitioners should be aware that, when omitting channel binding or accepting incorrect channel bindings, FIDO UAF is vulnerable to a protocol-interaction attack in which the adversary tricks the client and authenticator to act as confused deputies to sign an authentication challenge for the adversary. In addition to enabling the server to verify the client's binding of the challenge to the channel, our improved mandatory dual channel-binding mechanism provides the following two advantages: (1) By binding the challenge to the channel, the server provides an opportunity for the client to verify this binding. By contrast, in the current standard, the client cannot authenticate the server's challenge. (2) It performs binding at the server where the authentication challenge is created, hindering an adversary from transplanting the challenge into another protocol execution. Our case study illustrates the importance of cryptographically binding context to protocol messages to prevent an adversary from misusing messages out of context. 

We present a psychometric evaluation of the Cybersecurity Curriculum Assessment (CCA), completed by 193 students from seven colleges and universities. The CCA builds on our prior work developing and validating a Cybersecurity Concept Inventory (CCI), which measures students' conceptual understanding of cybersecurity after a first course in the area. The CCA deepens the conceptual complexity and technical depth expectations, assessing conceptual knowledge of students who had completed multiple courses in cybersecurity. We review our development of the CCA and present our evaluation of the instrument using Classical Test Theory and Item-Response Theory. The CCA is a difficult assessment, providing reliable measurements of student knowledge and deeper information about high-performing students. 

We present a psychometric evaluation of a revised version of the Cybersecurity Concept Inventory (CCI) , completed by 354 students from 29 colleges and universities. The CCI is a conceptual test of understanding created to enable research on instruction quality in cybersecurity education. This work extends previous expert review and small-scale pilot testing of the CCI. Results show that the CCI aligns with a curriculum many instructors expect from an introductory cybersecurity course, and that it is a valid and reliable tool for assessing what conceptual cybersecurity knowledge students learned. 

We explore shadow information technology (IT) at institutions of higher education through a two-tiered approach involving a detailed case study and comprehensive survey of IT professionals. In its many forms, shadow IT is the software or hardware present in a computer system or network that lies outside the typical review process of the responsible IT unit. We carry out a case study of an internally built legacy grants management system at the University of Maryland, Baltimore County that exemplifies the vulnerabilities, including cross-site scripting and SQL injection, typical of such unauthorized and ad-hoc software. We also conduct a survey of IT professionals at universities, colleges, and community colleges that reveals new and actionable information regarding the prevalence, usage patterns, types, benefits, and risks of shadow IT at their respective institutions. Further, we propose a security-based profile of shadow IT, involving a subset of elements from existing shadow IT taxonomies, which categorizes shadow IT from a security perspective. Based on this profile, survey respondents identified the predominant form of shadow IT at their institutions, revealing close similarities to findings from our case study. Through this work, we are the first to identify possible susceptibility factors associated with the occurrence of shadow IT related security incidents within academic institutions. Correlations of significance include the presence of certain graduate schools, the level of decentralization of the IT department, the types of shadow IT present, the percentage of security violations related to shadow IT, and the institution's overall attitude toward shadow IT. The combined elements of our case study, profile, and survey provide the first multifaceted view of shadow IT security at academic institutions, highlighting tension between its risks and benefits, and suggesting strategies for managing it successfully. 

We reflect on our ongoing journey in the educational Cybersecurity Assessment Tools (CATS) Project to create two concept inventories for cybersecurity. We identify key steps in this journey and important questions we faced. We explain the decisions we made and discuss the consequences of those decisions, highlighting what worked well and what might have gone better. The CATS Project is creating and validating two concept inventories—conceptual tests of understanding—that can be used to measure the effectiveness of various approaches to teaching and learning cybersecurity. The Cybersecurity Concept Inventory (CCI) is for students who have recently completed any first course in cybersecurity; the Cybersecurity Curriculum Assessment (CCA) is for students who have recently completed an undergraduate major or track in cybersecurity. Each assessment tool comprises 25 multiple-choice questions (MCQs) of various difficulties that target the same five core concepts, but the CCA assumes greater technical background. Key steps include defining project scope, identifying the core concepts, uncovering student misconceptions, creating scenarios, drafting question stems, developing distractor answer choices, generating educational materials, performing expert reviews, recruiting student subjects, organizing workshops, building community acceptance, forming a team and nurturing collaboration, adopting tools, and obtaining and using funding. Creating effective MCQs is difficult and time-consuming, and cybersecurity presents special challenges. Because cybersecurity issues are often subtle, where the adversarial model and details matter greatly, it is challenging to construct MCQs for which there is exactly one best but non-obvious answer. We hope that our experiences and lessons learned may help others create more effective concept inventories and assessments in STEM. 

We analyze the Secure Remote Password (SRP) protocol for structural weaknesses using the Cryptographic Protocol Shapes Analyzer (CPSA) in the first formal analysis of SRP (specifically, Version 3). SRP is a widely deployed Password Authenticated Key Exchange (PAKE) protocol used in 1Password, iCloud Keychain, and other products. As with many PAKE protocols, two participants use knowledge of a preshared password to authenticate each other and establish a session key. SRP aims to resist dictionary attacks, not store plaintext-equivalent passwords on the server, avoid patent infringement, and avoid export controls by not using encryption. Formal analysis of SRP is challenging in part because existing tools provide no simple way to reason about its use of the mathematical expression “v + g b mod q”. Modeling v + g b as encryption, we complete an exhaustive study of all possible execution sequences of SRP. Ignoring possible algebraic attacks, this analysis detects no major structural weakness, and in particular no leakage of any secrets. We do uncover one notable weakness of SRP, which follows from its design constraints. It is possible for a malicious server to fake an authentication session with a client, without the client’s participation. This action might facilitate an escalation of privilege attack, if the client has higher privileges than does the server. We conceived of this attack before we used CPSA and confirmed it by generating corresponding execution shapes using CPSA. 

We reflect on our ongoing journey in the educational Cybersecurity Assessment Tools (CATS) Project to create two concept inventories for cybersecurity. We identify key steps in this journey and important questions we faced. We explain the decisions we made and discuss the consequences of those decisions, highlighting what worked well and what might have gone better. The CATS Project is creating and validating two concept inventories—conceptual tests of understanding—that can be used to measure the effectiveness of various approaches to teaching and learning cybersecurity. The Cybersecurity Concept Inventory (CCI) is for students who have recently completed any first course in cybersecurity; the Cybersecurity Curriculum Assessment (CCA) is for students who have recently completed an undergraduate major or track in cybersecurity. Each assessment tool comprises 25 multiple-choice questions (MCQs) of various difficulties that target the same five core concepts, but the CCA assumes greater technical background. Key steps include defining project scope, identifying the core concepts, uncovering student misconceptions, creating scenarios, drafting question stems, developing distractor answer choices, generating educational materials, performing expert reviews, recruiting student subjects, organizing workshops, building community acceptance, forming a team and nurturing collaboration, adopting tools, and obtaining and using funding. Creating effective MCQs is difficult and time-consuming, and cybersecurity presents special challenges. Because cybersecurity issues are often subtle, where the adversarial model and details matter greatly, it is challenging to construct MCQs for which there is exactly one best but non-obvious answer. We hope that our experiences and lessons learned may help others create more effective concept inventories and assessments in STEM. 

We reflect on our ongoing journey in the educational Cybersecurity Assessment Tools (CATS) Project to create two concept inventories for cybersecurity. We identify key steps in this journey and important questions we faced. We explain the decisions we made and discuss the consequences of those decisions, highlighting what worked well and what might have gone better. The CATS Project is creating and validating two concept inventories---conceptual tests of understanding---that can be used to measure the effectiveness of various approaches to teaching and learning cybersecurity. The Cybersecurity Concept Inventory (CCI) is for students who have recently completed any first course in cybersecurity; the Cybersecurity Curriculum Assessment (CCA) is for students who have recently completed an undergraduate major or track in cybersecurity. Each assessment tool comprises 25 multiple-choice questions (MCQs) of various difficulties that target the same five core concepts, but the CCA assumes greater technical background. 

We analyze expert review and student performance data to evaluate the validity of the Cybersecurity Concept Inventory (CCI) for assessing student knowledge of core cybersecurity concepts after a first course on the topic. A panel of 12 experts in cybersecurity reviewed the CCI, and 142 students from six different institutions took the CCI as a pilot test. The panel reviewed each item of the CCI and the overwhelming majority rated every item as measuring appropriate cybersecurity knowledge. We administered the CCI to students taking a first cybersecurity course either online or proctored by the course instructor. We applied classical test theory to evaluate the quality of the CCI. This evaluation showed that the CCI is sufficiently reliable for measuring student knowledge of cybersecurity and that the CCI may be too difficult as a whole. We describe the results of the expert review and the pilot test and provide recommendations for the continued improvement of the CCI.